Skip to content

Verilog: implicit nets for concatenation members on continuous-assign LHS - #2164

Open
kroening wants to merge 1 commit into
mainfrom
kroening/typecheck-concat-implicit-net
Open

kroening wants to merge 1 commit into
mainfrom
kroening/typecheck-concat-implicit-net

Conversation

@kroening

Copy link
Copy Markdown
Collaborator

Split out from #2052 (root cause 2 of the LogikBench type-checker triage).

IEEE 1800-2017 6.10 declares an undeclared identifier used on the LHS of a continuous assignment as an implicit net of the default net type. convert_continuous_assign already handled this for a bare-identifier LHS but not when the identifier appeared as a member of a concatenation, e.g.

assign {cout, out} = a - b;   // cout is undeclared (discard-carry idiom)

which was rejected with "unknown identifier". Each undeclared bare-identifier member is now declared as a scalar net of the default net type before the concatenation is converted.

Fixes LogikBench arithmetic/sub. Adds regression test continuous_assign_implicit_net1.

make -C regression/verilog test passes.

🤖 Generated with Claude Code

… LHS

IEEE 1800-2017 6.10 declares an undeclared identifier used on the LHS of a
continuous assignment as an implicit net of the default net type.
convert_continuous_assign already did this for a bare-identifier LHS but not
when the identifier appeared as a member of a concatenation, e.g.

  assign {carry, sum} = a + b;   // carry is undeclared

which was rejected with "unknown identifier". Declare each undeclared
bare-identifier member as a scalar net before converting the concatenation.

Fixes LogikBench arithmetic/sub.

Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
Comment on lines +823 to +838
else if(lhs.id() == ID_concatenation)
{
// The implicit net rule also applies to undeclared identifiers that
// appear as members of a concatenation on the LHS, e.g.
// assign {carry, sum} = a + b; // carry is undeclared
// Declare each such member as a scalar net of the default net type,
// then convert the concatenation as usual.
for(auto &op : lhs.operands())
{
if(op.id() == ID_verilog_identifier)
op = convert_verilog_identifier(
to_verilog_identifier_expr(op), unsignedbv_typet{1});
}

convert_expr(lhs);
}

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Will we detect that there could be a lhs/rhs bit-width mismatch? It would be great to have a test covering this case.

This branch has not been deployed

No deployments
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants